package controller;

import java.util.Set;

import model.sequent.tokens.Atom;
import model.sequent.tokens.Expression;
import model.sequent.tokens.Sequent;
import controller.sequentParser.SequentParser;

/**
 * Algorithms & Data Structures - Exercise 5. Parses an arithmetic expression using the given parser from Blackboard and parses and evaluates a sequent using our own tail recursive sequent parser.
 * 
 * @author Sjaak Smetsers (number?)
 * @author Karen Berntsen (s0815799)
 * @author Erik Stens (s0615374)
 */
public class AD_exercise_5 {
	public static void main(String[] args) {
		// Exp arithmeticExpression = ArithmeticParser.parse("1 + -7 - -4 + 3 * 5");
		// System.out.printf("Result: %d\n", arithmeticExpression.eval());
		
		Sequent sequent = SequentParser.parse("A & !B | (A & BA & U | C > IMPL_a) & !!!(B = (C > E)), Y, P, Y @ D & !(A | B)");
		// Sequent sequent = SequentParser.parse("p | q @ p, q");
		// Sequent sequent = SequentParser.parse("p, q @ p & q");
		// Sequent sequent = SequentParser.parse("p > (q > r) @ (p > q) > r");
		// Sequent sequent = SequentParser.parse("p = q @ q = p");
		// Sequent sequent = SequentParser.parse("p | (q & r) @ (p | q) & (p | r)");
		// Sequent sequent = SequentParser.parse("p | q, !(p > q) @ (p & q) = p");
		
		if (sequent != null) {
			System.out.println("Sequent:");
			System.out.println(sequent);
		}
		
		Set<Sequent> reducedSequentSet = SequentEvaluator.reduceSequent(sequent);
		
		for (Sequent reducedSequent : reducedSequentSet) {
			System.out.println("\n\nReduced sequent: ");
			System.out.println(reducedSequent);
		}
		
		Set<Sequent> counterexampleSet = SequentEvaluator.evaluate(reducedSequentSet);
		
		if (counterexampleSet.isEmpty()) {
			System.out.println("\n\nResult of evaluation:\nNo valid solution could be found for the sequent.\nThis means the sequent is contradictory, so the original proposition from which the sequent was derived must be valid.");
		} else {
			System.out
					.println("\n\nResult of evaluation:\nOne or more valid solutions could be found for the sequent.\n\nThis means one or more counterexamples exist for the original proposition\nfrom which the sequent was derived, meaning this proposition is invalid.");
			System.out.println("\nCounterexamples to the original proposition:");
			
			int i = 1;
			for (Sequent counterexample : counterexampleSet) {
				System.out.println("\nCounterexample " + i++);
				System.out.println("True: " + getAtomString(counterexample.getTrueExpressionSet()));
				System.out.println("False: " + getAtomString(counterexample.getFalseExpressionSet()));
			}
		}
	}
	
	/**
	 * Builds a String that represents all the Atoms in an expressionSet. Separates the Atoms by commas.
	 * 
	 * @param expressionSet
	 * @return String
	 */
	private static String getAtomString(Set<Expression> expressionSet) {
		StringBuilder sb = new StringBuilder();
		boolean isFirst = true;
		for (Expression expression : expressionSet) {
			if (expression instanceof Atom) {
				Atom atom = (Atom) expression;
				if (!isFirst) {
					sb.append(", ");
				}
				sb.append(atom.getName());
				isFirst = false;
			}
		}
		return sb.toString();
	}
}
